ds,da,T:top, ks:(top List), upd:fpf((:Knd  Id); x.top), a:top, i,j:Id.
sqequal(R-has-loc(ecl-machine2(i; ds; da; mkid{ecl:ut2}; T; ks; a; upd); j);
sqequal(band((null(update-spec-vars(upd))); eq_id(i; j))) 

latex

Definitions	t  T, void, isect(A; x.B(x)), Id, Knd, x:A  B(x), x:A. B(x), fpf-domain(f), x:AB(x), x. t(x), t.2, x.A(x), map(f; as), P  Q, ecl-machine2(i; ds; da; x; T; ks; a; upd), fpf(A; a.B(a)), update-spec-vars(upd), top, type List, s = t, ff, , reduce(f; k; as), <a, b>, tt, band(p; q), prop{i:l}, b, Type, A, b, P  Q, P  Q, Unit, left + right, guard(T), sq_type(T), sqequal(s; t), eq_id(a; b)
Lemmas	bool sq, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bnot wf, not wf, assert wf, eq id wf, bool wf, btrue wf, bfalse wf, fpf wf, Rall-has-loc, R-state-var-loc, map wf, pi2 wf, fpf-domain wf, Knd wf, Id wf, top wf